Raframe(${\it loc}$; $k$; $L$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$inr inr inr inr inr inr inr inr (inl $<$${\it loc}$, $k$, $L$$>$ )